Knuth's up-arrow notation